\section{Future work}
As previously mentioned, we currently do not work directly on the abstract
syntax trees of the Scala compiler. The first and obvious next step we want to
take is to write a converter from that representation to our simplified one.
This would not only save us the cumbersome task of encoding examples manually,
	 but would also be a first step towards a release of this project as a
	 \texttt{scalac} plugin. 

The current system could also be improved to correctly cope with more cases:
\begin{itemize}

\item We would like to deal with more primitive types than just integers.

\item {Scala allows for matching on Strings. We currently do
	not support this, but we believe it would be fairly easy to implement.
			String constants can simply be replaced by fresh variable names.
			Comparison would hence be dealt with correctly. Note that this is
			in essence similar to the constant pool in Java classes, which is
			precisely the mechanism which makes comparison between String
			constants work properly, even using \texttt{==}.

			This would allow the following example to be proved to be complete and disjoint:
\begin{lstlisting}
s: String match {
    case "Hello" $\Rightarrow$ $\ldots$
    case t: String if(!t.equals("Hello")) $\Rightarrow$ $\ldots$
}
\end{lstlisting}
}

\item {We've mentioned that we simply ignore most of the method calls in the
guards. We could refine this by examining the return type of these method
calls, and then replacing them by a fresh variable of that type. The following
example could be declared complete and disjoint:

\begin{lstlisting}
t: Tree match {
    case _ if(t.isBalanced) $\Rightarrow$ $\ldots$
    case _ if(!t.isBalanced) $\Rightarrow$ $\ldots$
}
\end{lstlisting}

The expression \texttt{t.isBalanced} would be detected in both patterns as the
same boolean expression. It would in turn be replaced by a fresh variable of
that type, and the correctness of the proof would be ensured by an axiom
stating that a boolean is either true or false. The same mechanism can be
applied to primitive types, and even to user-defined types, as long the
hierarchy is completely known.

Notice that we have only mentioned method calls here, but variables which are
defined outside of the matching expression can be treated similarly; if we know
their type, we can apply the same procedure.
}

\end{itemize}

At some point we would also like to formally prove the soundness of our
approach. Indeed, the transformations we apply to patterns to generate formulae
are only intuitively correct, and even though experiments have always validated
our assumptions so far, we still lack the confidence that everything we did
is correct.

One last thing we would definitely like to do before releasing and supporting a
plugin, is a ``call for patterns''. We would be interested in conducting a
survey, for instance via the Scala mailing lists, to know what people commonly
write as pattern matching expressions. This would be an efficient way of
collecting many examples to test, and would give us further confidence that the
limitations of our implementation are not a major drawback in most practical
applications.
